(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun mem_35_115 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun mem_35_111 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun mem_35_109 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun t_108 () (_ BitVec 1))
(declare-fun t_107 () (_ BitVec 1))
(declare-fun t_106 () (_ BitVec 1))
(declare-fun t_105 () (_ BitVec 1))
(declare-fun t_104 () (_ BitVec 1))
(declare-fun t_103 () (_ BitVec 1))
(declare-fun t_102 () (_ BitVec 1))
(declare-fun t_101 () (_ BitVec 1))
(declare-fun t_100 () (_ BitVec 1))
(declare-fun ra_final_56_99 () (_ BitVec 32))
(declare-fun T_32t1_608_96 () (_ BitVec 32))
(declare-fun T_32t2_614_90 () (_ BitVec 32))
(declare-fun T_32t3_618_86 () (_ BitVec 32))
(declare-fun T_32t1_616_85 () (_ BitVec 32))
(declare-fun T_32t2_622_79 () (_ BitVec 32))
(declare-fun ra0_57_76 () (_ BitVec 32))
(declare-fun R_EBP_0_60 () (_ BitVec 32))
(declare-fun R_ESP_1_58 () (_ BitVec 32))
(assert (= (_ bv1 1) (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (ite (= t_108 (ite (= ra0_57_76 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_109 (bvadd R_ESP_1_58 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_109 (bvadd R_ESP_1_58 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_109 (bvadd R_ESP_1_58 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_109 (bvadd R_ESP_1_58 (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (ite (= t_107 (ite (= T_32t2_622_79 (bvsub R_ESP_1_58 (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_106 (ite (= mem_35_111 (store (store (store (store mem_35_109 (bvadd T_32t2_622_79 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv24 32)))) (bvadd T_32t2_622_79 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv16 32)))) (bvadd T_32t2_622_79 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv8 32)))) (bvadd T_32t2_622_79 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_60))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_105 (ite (= T_32t1_616_85 (bvadd T_32t2_622_79 (_ bv8 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_104 (ite (= T_32t3_618_86 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_111 (bvadd T_32t1_616_85 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_111 (bvadd T_32t1_616_85 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_111 (bvadd T_32t1_616_85 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_111 (bvadd T_32t1_616_85 (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_103 (ite (= T_32t2_614_90 (bvadd T_32t2_622_79 (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_102 (ite (= mem_35_115 (store (store (store (store mem_35_111 (bvadd (_ bv134527924 32) (_ bv3 32)) ((_ extract 7 0) (bvlshr T_32t3_618_86 (_ bv24 32)))) (bvadd (_ bv134527924 32) (_ bv2 32)) ((_ extract 7 0) (bvlshr T_32t3_618_86 (_ bv16 32)))) (bvadd (_ bv134527924 32) (_ bv1 32)) ((_ extract 7 0) (bvlshr T_32t3_618_86 (_ bv8 32)))) (bvadd (_ bv134527924 32) (_ bv0 32)) ((_ extract 7 0) T_32t3_618_86))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_101 (ite (= T_32t1_608_96 (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_115 (bvadd T_32t2_614_90 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_115 (bvadd T_32t2_614_90 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_115 (bvadd T_32t2_614_90 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_115 (bvadd T_32t2_614_90 (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (ite (= t_100 (ite (= ra_final_56_99 T_32t1_608_96) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))) (bvand (bvnot (_ bv0 1)) (bvand (bvand t_108 (bvand t_107 (bvand t_106 (bvand t_105 (bvand t_104 (bvand t_103 (bvand t_102 (bvand t_101 t_100)))))))) (ite (not (= ra0_57_76 ra_final_56_99)) (_ bv1 1) (_ bv0 1)))))))
(check-sat)
(set-option :regular-output-channel "/dev/null")
(get-model)
(exit)
